R-base-ma(R)
== case R of 
== Rnone => 
== Rplus(left,right)=>rec1,rec2.
== Rinit(loc,T,x,v)=> x : T initially x = v
== Rframe(loc,T,x,L)=> only members of L affect x :T
== Rsframe(lnk,tag,L)=> only L sends on (lnk with tag)
== Reffect(loc,ds,knd,T,x,f)=> with declarations 
== ds:ds
== da:knd : T
== effect of knd(v) is x := f s v
== Rsends(ds,knd,T,l,dt,g)=> with declarations 
== ds:ds
== da:knd : T  lnk-decl(l;dt)
== knd(v) sends g s v on link l
== Rpre(loc,ds,a,T,P)=> (with ds: ds
== Raction a:T
== Rprecondition a(v) is
== RP s v)
== Raframe(loc,k,L)=> k affects only members of L
== Rbframe(loc,k,L)=> k sends only on links in L
== Rrframe(loc,x,L)=> only members of L read x 

latex

---

clarification:

R-base-ma(R)
== case R of 
== Rnone => 
== Rplus(left,right)=>rec1,rec2.
== Rinit(loc,T,x,v)=> x : T initially x = v
== Rframe(loc,T,x,L)=> only members of L affect x :T
== Rsframe(lnk,tag,L)=> only L sends on (lnk with tag)
== Reffect(loc,ds,knd,T,x,f)=> with declarations 
== ds:ds
== da:knd : T
== effect of knd(v) is x := f s v
== Rsends(ds,knd,T,l,dt,g)=> with declarations 
== ds:ds
== da:fpf-join(KindDeq;knd : T;lnk-decl(l;dt))
== knd(v) sends g s v on link l
== Rpre(loc,ds,a,T,P)=> (with ds: ds
== Raction a:T
== Rprecondition a(v) is
== RP s v)
== Raframe(loc,k,L)=> k affects only members of L
== Rbframe(loc,k,L)=> k sends only on links in L
== Rrframe(loc,x,L)=> only members of L read x 

latex

Definitions	es realizer ind, , x : t initially x = v, only members of L affect x :t, only L sends on (l with tg), with declarations ds:dsda:daeffect of k(v) is x := f s v, with declarations ds:dsda:dak(v) sends f s v on link l, f  g, KindDeq, x : v, lnk-decl(l;dt), (with ds: ds action a:T precondition a(v) is P s v), k affects only members of L, k sends only on links in L, only members of L read x
FDL editor aliases	R-base-ma